(*
** Algunos ejemplos sobre como utilizar la sintaxis del lenguaje.
*)

Require Import TypesImpl.
Open Scope Z_scope.
Open Scope lang_scope.

Definition arith_exp_example(x y: Id) :=
  int x ::= 3 + y;
  int y ::= x - y / 2;
  int x ::= x + y * 3;
  int y ::= x mod 2;
.

Definition bool_exp_example(a b x y: Id) :=
  bool a ::= !a and b or FALSE;
  bool b ::= (x le y) or (y == 4);
.

Definition byte_exp_example(s t matr: Id) :=
  byte s ::= t shl 3;
  byte t ::= s xor 2;
  byte s ::= (t band s) shr 2;
  byte t ::= matr[1][1] band matr[2][2];
. 

Definition matrix_set_example(matr i j: Id) :=
  matr[1][1] ::= 3;
  matr[i+j][i+1] ::= 3;
  matr[1][1] ::= matr[3][1] shl 3;
.

Definition if_example(cond1 cond2 n: Id) :=
  bool cond1 ::= TRUE;
  bool cond2 ::= FALSE;

  IFB cond1 or cond2 THEN
    int n ::= 3;
  END
.

Definition while_example(it max: Id) :=
  int it ::= 0;
  int max ::= 2;

  WHILE it lt 2 DO
    int it ::= it + 1;
  END
.

Definition for_example(var: Id) :=
  int var ::= 0;

  FOR var TO 3 DO
    int var ::= var + 1;
  END
.